|
|
Static Analyzer for List Manipulating Programs
Kotoun, Michal ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.
|
|
|
Methods for Analysis of Switched Circuits
Kovář, Jan ; Ondráček, Oldřich (referee) ; Kalous, Jaroslav (referee) ; Kolka, Zdeněk (advisor)
The dissertation deals with simulations of the DC-DC converters in their basic configurations (Buck, Boost, Buck-boost, Cuk, SEPIC). In the first part of the thesis derivation of transfer functions Line-to-Output (LTO) and Control-To-Output (CTO) can be found. These symbolic responses are derived for three types of basic converters (Buck, Boost, Buck-boost) using well-known average model [1]. Derived expressions are very complicated. For reduction of these expressions symbolic approximation method was used, however the generality is lost. The average model was used to for decreasing the computational effort of analysis of DC-DC converters in the time domain. For these simulations VHDL-AMS language was used. The main topic of the thesis is harmonic balance method, which was adapted to DC-DC converters. Because conditions and assumptions for LTO and CTO functions are very different, harmonic balance method was derived into two variants. For obtaining of LTO response, duty cycle of switching signal can be considered as constant in time. Spectrum of this signal is simple as follows from well-known sinc function. For obtaining of CTO response PWM modulation must be used. Compared to sinc function spectrum of PWM modulation is richer (contains more combination frequencies). Many types of PWM modulation is described in [31]. For simulation PWM modulation with uniform sampling in two variants (single and double edge) was used. Non-ideal switching of PWM switch was modeled by PWM pulse with defined slew rate. Last section deals with comparison of all derived functions (LTO, CTO, modulation type, defined slew rate) with well-known averaged model.
|
|
|
Static Analyzer for List Manipulating Programs
Kotoun, Michal ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.
|
|
|
Methods for Analysis of Switched Circuits
Kovář, Jan ; Ondráček, Oldřich (referee) ; Kalous, Jaroslav (referee) ; Kolka, Zdeněk (advisor)
The dissertation deals with simulations of the DC-DC converters in their basic configurations (Buck, Boost, Buck-boost, Cuk, SEPIC). In the first part of the thesis derivation of transfer functions Line-to-Output (LTO) and Control-To-Output (CTO) can be found. These symbolic responses are derived for three types of basic converters (Buck, Boost, Buck-boost) using well-known average model [1]. Derived expressions are very complicated. For reduction of these expressions symbolic approximation method was used, however the generality is lost. The average model was used to for decreasing the computational effort of analysis of DC-DC converters in the time domain. For these simulations VHDL-AMS language was used. The main topic of the thesis is harmonic balance method, which was adapted to DC-DC converters. Because conditions and assumptions for LTO and CTO functions are very different, harmonic balance method was derived into two variants. For obtaining of LTO response, duty cycle of switching signal can be considered as constant in time. Spectrum of this signal is simple as follows from well-known sinc function. For obtaining of CTO response PWM modulation must be used. Compared to sinc function spectrum of PWM modulation is richer (contains more combination frequencies). Many types of PWM modulation is described in [31]. For simulation PWM modulation with uniform sampling in two variants (single and double edge) was used. Non-ideal switching of PWM switch was modeled by PWM pulse with defined slew rate. Last section deals with comparison of all derived functions (LTO, CTO, modulation type, defined slew rate) with well-known averaged model.
|
guest ::
